Sable Debug

LTL: G(((!g_0 & !g_1 & (!g_2 | !g_3)) | (!g_2 & !g_3 & (!g_0 | !g_1))) & (r_0 -> Fg_0) & (r_1 -> Fg_1) & (r_2 -> Fg_2) & (r_3 -> Fg_3))

Input APs: [r_0, r_1, r_2, r_3]

Illegal letters: 176 out of the 256 letters (68.75%) are illegal.

¬LTL: !G(((!g_0 & !g_1 & (!g_2 | !g_3)) | (!g_2 & !g_3 & (!g_0 | !g_1))) & (r_0 -> Fg_0) & (r_1 -> Fg_1) & (r_2 -> Fg_2) & (r_3 -> Fg_3))

NonDet Buchi of negated LTL:

Universal CoBuchi of LTL:

Starting with K = 0

Expanded K-CoBuchi for K=0:

kUCB complement:

The empty word is accepted.

LSafe iteration #1

Closing table ...

Hypothesis table:

Table:
  0: 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []

Number of states: 2

Hypothesis is NOT realisable.

Strategy:

Moore machine:

No counterexample found. For this K, the formula is not realisable.

Timers for K = 0:

We have a proof of unrealisability for K = 0

However this is not a proof for the general formula. We need to increment K.

Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & !r_0 & !r_1 & r_2 & r_3}

Incrementing K to 1

Expanded K-CoBuchi for K=1:

kUCB complement:

The empty word is accepted.

LSafe iteration #1

Closing table ...

Hypothesis table:

Table:
  0: 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []

Number of states: 2

Hypothesis is realisable.

Strategy:

Mealy machine 1:

Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}

Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

LSafe iteration #2

Closing table ...

Hypothesis table:

Table:
  0: 1 1 
  2: 1 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Number of states: 3

Hypothesis is realisable.

Strategy:

Mealy machine 2:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}

Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 
  2: 1 0 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

LSafe iteration #3

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 
  4: 1 1 0 
  2: 1 0 1 
  3: 1 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Number of states: 5

Hypothesis is realisable.

Strategy:

Mealy machine 4:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 
  4: 1 1 0 0 
  2: 1 0 1 0 
  3: 1 0 0 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  3: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

LSafe iteration #4

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 
  4: 1 1 0 0 
  2: 1 0 1 0 
  3: 1 0 0 1 
  5: 1 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  3: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Number of states: 6

Hypothesis is NOT realisable.

Strategy:

Moore machine:

No counterexample found. For this K, the formula is not realisable.

Timers for K = 1:

We have a proof of unrealisability for K = 1

However this is not a proof for the general formula. We need to increment K.

Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & !r_0 & r_1 & r_2 & r_3}

Incrementing K to 2

Expanded K-CoBuchi for K=2:

kUCB complement:

The empty word is accepted.

LSafe iteration #1

Closing table ...

Hypothesis table:

Table:
  0: 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []

Number of states: 2

Hypothesis is realisable.

Strategy:

Mealy machine 1:

Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}

Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

LSafe iteration #2

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 
  2: 1 0 1 
  3: 1 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Number of states: 4

Hypothesis is realisable.

Strategy:

Mealy machine 3:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}

Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 
  2: 1 0 1 1 1 
  3: 1 0 0 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

LSafe iteration #3

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 
  5: 1 1 1 0 1 
  9: 1 1 1 0 0 
  8: 1 1 0 0 0 
  2: 1 0 1 1 1 
  4: 1 0 1 0 1 
 10: 1 0 1 0 0 
  3: 1 0 0 1 1 
  6: 1 0 0 0 1 
  7: 1 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Number of states: 11

Hypothesis is realisable.

Strategy:

Mealy machine 10:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 
  9: 1 1 1 0 0 0 0 
  8: 1 1 0 0 0 0 0 
  2: 1 0 1 1 1 0 1 
  4: 1 0 1 0 1 1 1 
 10: 1 0 1 0 0 0 0 
  3: 1 0 0 1 1 0 0 
  6: 1 0 0 0 1 0 0 
  7: 1 0 0 0 0 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

LSafe iteration #4

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 
  9: 1 1 1 0 0 0 0 
  8: 1 1 0 0 0 0 0 
  2: 1 0 1 1 1 0 1 
  4: 1 0 1 0 1 1 1 
 11: 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 
  3: 1 0 0 1 1 0 0 
  6: 1 0 0 0 1 0 0 
  7: 1 0 0 0 0 1 1 
 12: 1 0 0 0 0 0 1 
 13: 1 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Number of states: 14

Hypothesis is realisable.

Strategy:

Mealy machine 12:

Original (symbolic) counterexample: cycle{g_0 & !g_1 & !g_2 & !g_3 & r_2; !g_0 & g_1 & !g_2 & !g_3 & !r_2 & r_3}

Counterexample: cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3}

Shortest finite counterexample: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 
  9: 1 1 1 0 0 0 0 0 0 
  8: 1 1 0 0 0 0 0 0 0 
  2: 1 0 1 1 1 0 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 
 10: 1 0 1 0 0 0 0 0 0 
  3: 1 0 0 1 1 0 0 0 1 
  6: 1 0 0 0 1 0 0 0 1 
  7: 1 0 0 0 0 1 1 1 0 
 12: 1 0 0 0 0 0 1 1 0 
 13: 1 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]

LSafe iteration #5

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 
  9: 1 1 1 0 0 0 0 0 0 
  8: 1 1 0 0 0 0 0 0 0 
  2: 1 0 1 1 1 0 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 
 14: 1 0 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 0 0 
  3: 1 0 0 1 1 0 0 0 1 
  6: 1 0 0 0 1 0 0 0 1 
  7: 1 0 0 0 0 1 1 1 0 
 12: 1 0 0 0 0 0 1 1 0 
 15: 1 0 0 0 0 0 1 0 0 
 13: 1 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]

Number of states: 16

Hypothesis is NOT realisable.

Strategy:

Moore machine:

Counterexample: !g_0 & !g_1 & g_2 & !g_3 & !r_0 & r_1 & r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & r_1 & r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 
  8: 1 1 0 0 0 0 0 0 0 0 1 
  2: 1 0 1 1 1 0 1 1 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 
  3: 1 0 0 1 1 0 0 0 1 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

LSafe iteration #6

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 
  8: 1 1 0 0 0 0 0 0 0 0 1 
  2: 1 0 1 1 1 0 1 1 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 
  3: 1 0 0 1 1 0 0 0 1 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

Number of states: 18

Hypothesis is NOT realisable.

Strategy:

Moore machine:

Counterexample: g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3; !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}

Shortest finite counterexample: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

LSafe iteration #7

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Number of states: 21

Hypothesis is NOT realisable.

Strategy:

Moore machine:

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

LSafe iteration #8

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 
 21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 
 22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 
 23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Number of states: 24

Hypothesis is NOT realisable.

Strategy:

Moore machine:

Counterexample: !g_0 & !g_1 & g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 
 21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 
 22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 
 23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

LSafe iteration #9

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 
 21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 
 22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 
 24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 
 23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 
 25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
 25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]

Number of states: 26

Hypothesis is NOT realisable.

Strategy:

Moore machine:

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3; !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3; g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3; !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 0 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 0 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 1 0 1 
 21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 0 1 
 22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 0 1 
 24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 1 
 23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 1 
 25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
 25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 19: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

LSafe iteration #10

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 1 
  5: 1 1 1 0 1 0 1 0 1 1 1 0 1 1 1 1 1 0 1 1 
  9: 1 1 1 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1 
  8: 1 1 0 0 0 0 0 0 0 0 1 0 0 1 0 1 0 0 0 1 
  2: 1 0 1 1 1 0 1 1 1 0 1 0 1 0 1 1 1 1 1 1 
  4: 1 0 1 0 1 1 1 1 1 1 1 1 1 0 1 0 1 0 0 1 
 11: 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 1 0 0 1 
 16: 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 1 0 0 1 
 14: 1 0 1 0 1 0 1 0 1 0 1 1 1 1 1 0 1 1 0 1 
 21: 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 1 0 0 1 
 22: 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 0 0 1 
 24: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 1 0 1 1 
 18: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 1 0 1 
 26: 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 1 0 0 1 
 23: 1 0 1 0 0 0 0 0 0 0 1 0 0 1 0 0 0 0 0 1 
 10: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 1 0 0 0 1 
 25: 1 0 1 0 0 0 0 0 0 0 1 0 0 0 0 0 0 0 0 1 
  3: 1 0 0 1 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0 
 27: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 1 0 
  6: 1 0 0 0 1 0 0 0 1 0 0 0 0 0 0 0 1 0 0 0 
  7: 1 0 0 0 0 1 1 1 0 1 0 1 0 0 0 0 0 0 0 0 
 12: 1 0 0 0 0 0 1 1 0 0 0 0 0 0 0 0 0 0 0 0 
 17: 1 0 0 0 0 0 1 0 0 1 0 0 0 0 0 0 0 0 0 0 
 15: 1 0 0 0 0 0 1 0 0 0 0 1 0 0 0 0 0 0 0 0 
 19: 1 0 0 0 0 0 1 0 0 0 0 0 0 0 0 0 0 0 0 0 
 20: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 1 0 0 
 28: 1 0 0 0 0 0 0 0 0 0 0 0 1 0 1 0 0 0 0 0 
 13: 1 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
 25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
 26: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & !r_3]
 27: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
 28: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  8: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & r_2 & r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 10: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 11: [!g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 12: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 14: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 16: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 18: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]
 19: [!g_0 & !g_1 & !g_2 & g_3 & !r_0 & !r_1 & !r_2 & r_3]

Number of states: 29

Hypothesis is NOT realisable.

Strategy:

Moore machine:

No counterexample found. For this K, the formula is not realisable.

Timers for K = 2:

We have a proof of unrealisability for K = 2

However this is not a proof for the general formula. We need to increment K.

Counterexample: cycle{!g_0 & !g_1 & g_2 & g_3 & r_0 & r_1 & r_2 & r_3}

Incrementing K to 3

Expanded K-CoBuchi for K=3:

kUCB complement:

The empty word is accepted.

LSafe iteration #1

Closing table ...

Hypothesis table:

Table:
  0: 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []

Number of states: 2

Hypothesis is realisable.

Strategy:

Mealy machine 1:

Original (symbolic) counterexample: cycle{!g_0 & !g_1 & !g_2 & r_0}

Counterexample: cycle{!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

LSafe iteration #2

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 
  2: 1 0 1 1 
  4: 1 0 0 1 
  3: 1 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]

Number of states: 5

Hypothesis is realisable.

Strategy:

Mealy machine 4:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & r_1; cycle{g_0 & !g_1 & !g_2 & !g_3 & !r_1 & !r_2}

Counterexample: !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3; cycle{g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 
  2: 1 0 1 1 1 1 1 
  4: 1 0 0 1 1 1 1 
  3: 1 0 0 0 1 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

LSafe iteration #3

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 
  6: 1 1 1 1 0 1 1 
 12: 1 1 1 1 0 0 1 
 15: 1 1 1 1 0 0 0 
 11: 1 1 0 0 0 0 0 
  2: 1 0 1 1 1 1 1 
  5: 1 0 1 1 0 1 1 
 13: 1 0 1 1 0 0 1 
 16: 1 0 1 1 0 0 0 
  4: 1 0 0 1 1 1 1 
  7: 1 0 0 1 0 1 1 
 10: 1 0 0 1 0 0 1 
 17: 1 0 0 1 0 0 0 
  3: 1 0 0 0 1 1 1 
  8: 1 0 0 0 0 1 1 
 14: 1 0 0 0 0 0 1 
  9: 1 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]

Number of states: 18

Hypothesis is realisable.

Strategy:

Mealy machine 17:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_2 & !r_3}

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 
  6: 1 1 1 1 0 1 1 0 1 1 
 12: 1 1 1 1 0 0 1 0 0 1 
 15: 1 1 1 1 0 0 0 0 0 0 
 11: 1 1 0 0 0 0 0 0 0 1 
  2: 1 0 1 1 1 1 1 0 1 1 
  5: 1 0 1 1 0 1 1 1 1 1 
 13: 1 0 1 1 0 0 1 0 0 1 
 16: 1 0 1 1 0 0 0 0 0 0 
  4: 1 0 0 1 1 1 1 0 0 1 
  7: 1 0 0 1 0 1 1 0 0 1 
 10: 1 0 0 1 0 0 1 1 1 1 
 17: 1 0 0 1 0 0 0 0 0 0 
  3: 1 0 0 0 1 1 1 0 0 1 
  8: 1 0 0 0 0 1 1 0 0 0 
 14: 1 0 0 0 0 0 1 0 0 0 
  9: 1 0 0 0 0 0 0 1 1 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

LSafe iteration #4

Closing table ...

Hypothesis table:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 
  6: 1 1 1 1 0 1 1 0 1 1 
 12: 1 1 1 1 0 0 1 0 0 1 
 15: 1 1 1 1 0 0 0 0 0 0 
 11: 1 1 0 0 0 0 0 0 0 1 
 23: 1 1 0 0 0 0 0 0 0 0 
  2: 1 0 1 1 1 1 1 0 1 1 
  5: 1 0 1 1 0 1 1 1 1 1 
 18: 1 0 1 1 0 1 1 0 1 1 
 13: 1 0 1 1 0 0 1 0 0 1 
 16: 1 0 1 1 0 0 0 0 0 0 
  4: 1 0 0 1 1 1 1 0 0 1 
  7: 1 0 0 1 0 1 1 0 0 1 
 10: 1 0 0 1 0 0 1 1 1 1 
 20: 1 0 0 1 0 0 1 0 1 1 
 24: 1 0 0 1 0 0 1 0 0 1 
 17: 1 0 0 1 0 0 0 0 0 0 
  3: 1 0 0 0 1 1 1 0 0 1 
 19: 1 0 0 0 1 1 1 0 0 0 
  8: 1 0 0 0 0 1 1 0 0 0 
 14: 1 0 0 0 0 0 1 0 0 0 
  9: 1 0 0 0 0 0 0 1 1 1 
 22: 1 0 0 0 0 0 0 0 1 1 
 25: 1 0 0 0 0 0 0 0 0 1 
 21: 1 0 0 0 0 0 0 0 0 0 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]

Number of states: 26

Hypothesis is realisable.

Strategy:

Mealy machine 25:

Original (symbolic) counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3; !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3; g_0 & !g_1 & !g_2 & !g_3 & !r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & !r_2 & r_3}

Counterexample: !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3; !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3; cycle{!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3; g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3; !g_0 & g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3}

Shortest finite counterexample: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]

Adding all suffixes of the counterexample to S.

Table after accounting for counterexample:

Table:
  0: 1 1 1 1 1 1 1 1 1 1 1 1 1 
  6: 1 1 1 1 0 1 1 0 1 1 0 1 1 
 12: 1 1 1 1 0 0 1 0 0 1 0 0 1 
 15: 1 1 1 1 0 0 0 0 0 0 0 0 0 
 11: 1 1 0 0 0 0 0 0 0 1 0 0 1 
 23: 1 1 0 0 0 0 0 0 0 0 0 0 0 
  2: 1 0 1 1 1 1 1 0 1 1 1 1 1 
  5: 1 0 1 1 0 1 1 1 1 1 0 1 1 
 18: 1 0 1 1 0 1 1 0 1 1 0 1 1 
 13: 1 0 1 1 0 0 1 0 0 1 0 0 1 
 16: 1 0 1 1 0 0 0 0 0 0 0 0 0 
  4: 1 0 0 1 1 1 1 0 0 1 0 1 1 
  7: 1 0 0 1 0 1 1 0 0 1 0 1 1 
 10: 1 0 0 1 0 0 1 1 1 1 0 0 1 
 20: 1 0 0 1 0 0 1 0 1 1 0 0 1 
 24: 1 0 0 1 0 0 1 0 0 1 0 0 1 
 17: 1 0 0 1 0 0 0 0 0 0 0 0 0 
  3: 1 0 0 0 1 1 1 0 0 1 0 1 1 
 19: 1 0 0 0 1 1 1 0 0 0 0 0 1 
  8: 1 0 0 0 0 1 1 0 0 0 0 0 1 
 14: 1 0 0 0 0 0 1 0 0 0 0 0 1 
  9: 1 0 0 0 0 0 0 1 1 1 0 0 1 
 22: 1 0 0 0 0 0 0 0 1 1 0 0 0 
 25: 1 0 0 0 0 0 0 0 0 1 0 0 0 
 21: 1 0 0 0 0 0 0 0 0 0 0 0 1 
  1: 0 

Prefixes:
  0: []
  1: [g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  2: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
  3: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  4: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
  5: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  6: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 12: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 13: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 14: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 15: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 16: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 17: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 18: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3]
 19: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 20: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 21: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 22: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3]
 23: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 24: [!g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]
 25: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & !r_3, !g_0 & !g_1 & g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3]

Suffixes:
  0: []
  1: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  2: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3, !g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  3: [!g_0 & !g_1 & !g_2 & g_3 & r_0 & r_1 & r_2 & r_3]
  4: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  5: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  6: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & !r_1 & !r_2 & r_3]
  7: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  8: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3, !g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
  9: [!g_0 & g_1 & !g_2 & !g_3 & !r_0 & r_1 & !r_2 & !r_3]
 10: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & r_3, !g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
 11: [!g_0 & !g_1 & !g_2 & !g_3 & !r_0 & !r_1 & !r_2 & !r_3, g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]
 12: [g_0 & !g_1 & !g_2 & !g_3 & r_0 & r_1 & !r_2 & r_3]

LSafe iteration #5

Closing table ...